A:Type, I:MaInterface(A). Normal(A,I)   

latex

Definitions	x:A. B(x), t  T, , Normal(A,I), P & Q, P  Q, S  T
Lemmas	normal-type wf, Id wf, l member wf, ma-interface-locs wf, normal-ds wf, ma-interface-ds wf, Knd wf, ma-interface-dom wf, assert wf, hasloc wf, ma-interface-valtype wf, ma-interface wf